Inference at * 3 1 
Iof proof for Lemma not over or:



1. A : 
2. B : 
3. (A) & (B)
4. A  B
  False 

latex

 by ((((D 4) 
CollapseTHEN (D 3))) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 4:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

P  Q, False, P  Q, A, P & Q